a,b:, E:(int_seg(a; b)rationals). qsum(a; b; j.E(j))  rationals 

latex

Definitions	t.1, x. t(x), rng_car(r), qrng, x(s), qsum(a; b; j.E(j)), t  T, x:A. B(x), crng{i:l}, rng{i:l}
Lemmas	rng car wf, int seg wf, rationals wf, crng wf, qrng wf, rng sum wf